COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	A formal theory %eT%* is defined when the following conditions are
C00005 ENDMK
C⊗;
A formal theory %eT%* is defined when the following conditions are
satisfied⊗↓See page {yon(P1)} for propositional logic as a formal 
theory.←:

.BEGIN INDENT 5,5,5;

%21.%*  A countable set of symbols is  given as the symbols of %eT%*.
A finite sequence of symbols of %eT%* is called an expression of %eT%*.

%22.%* There is a subset of the expressions of %eT%* called the %3well-formed
formulas%* (abbreviated %3wffs%*) of %eT%*⊗↓Ther is usually
an effective procedure to determine whether a given expression is a  wff.←.

%23.%* A set of wffs is set aside and cslled the set of %3axioms%*
of %eT%*⊗↓%eT%* is an axiomatic theory if there exists an effective
procedure for deciding whether a given wff is an axiom.←.

%24.%* Ther is a finite set of relations %eR%41%1,#...#,%eR%4n%1 on
wffs, called %3rules of inference%*. For each %eR%4i%1 there is a unique
positve integer %ej%* such that for every set of %ej%* wffs and each wff
%dA%* one can effectively decise whether the  given %ej%* wffs are in the
relation %eR%4i%1 to %dA%*, and, if so %dA%* is called a %3direct consequence%*
of the given wffs by virtue of %eR%4i%1.
.END

Let %gG%* be a set of wffs, and let %dP%* be a wff in the formal theory %eT%*.
We say %dP%3 is deducible for %gG%1 (denoted %gG%5ε%dP%1) 
if there exists a finite sequence of wffs
%dP%41%1,#...,#%dP%4n%1 such that %dP%4n%1#=#%dP%1 and for 1≤i≤n, %dP%4i%1
is either an axiom, a formula in %gG%* is a direct